Solving Mixed Quantified Constraints over a Domain Based on $$\mathcal{R}$$eal Numbers and $$\mathcal{H}$$erbrand Terms
Identifieur interne : 008741 ( Main/Exploration ); précédent : 008740; suivant : 008742Solving Mixed Quantified Constraints over a Domain Based on $$\mathcal{R}$$eal Numbers and $$\mathcal{H}$$erbrand Terms
Auteurs : Miguel García-Díaz [Espagne] ; Susana Nieva [Espagne]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Combining the logic of hereditary Harrop formulas HH with a constraint system, a logic programming language is obtained that extends Horn clauses in two different directions, thus enhancing substantially the expressivity of Prolog. The implementation of this new language requires the ability to test the satisfiability of constraints built up by means of terms and predicates belonging to the domain of the chosen constraint system, and by the connectives and quantifiers usual in first-order logic. In this paper we present a constraint system called $$ \mathcal{R}\mathcal{H} $$ for a hybrid domain that mixes Herbrand terms and real numbers. It arises when joining the axiomatization of the arithmetic of real numbers and the axiomatization of the algebra of finite trees. We have defined an algorithm to solve certain constraints of this kind. The novelty relies on the combination of two different mechanisms, based on elimination of quantifiers, o ne used for solving unification and disunification problems, the other used to solve polynomials. This combination provides a procedure to solve $$ \mathcal{R}\mathcal{H} $$ -constraints in the context of HH with constraints.
Url:
DOI: 10.1007/3-540-45788-7_6
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 000F38
- to stream Istex, to step Curation: 000F24
- to stream Istex, to step Checkpoint: 001B77
- to stream Main, to step Merge: 008B97
- to stream Main, to step Curation: 008741
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Solving Mixed Quantified Constraints over a Domain Based on $$\mathcal{R}$$eal Numbers and $$\mathcal{H}$$erbrand Terms</title><author><name sortKey="Garcia Diaz, Miguel" sort="Garcia Diaz, Miguel" uniqKey="Garcia Diaz M" first="Miguel" last="García-Díaz">Miguel García-Díaz</name></author><author><name sortKey="Nieva, Susana" sort="Nieva, Susana" uniqKey="Nieva S" first="Susana" last="Nieva">Susana Nieva</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:41410A90B5254E892607C6E4FF45F4FAC578309C</idno><date when="2002" year="2002">2002</date><idno type="doi">10.1007/3-540-45788-7_6</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-W9M5NXP5-X/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000F38</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000F38</idno><idno type="wicri:Area/Istex/Curation">000F24</idno><idno type="wicri:Area/Istex/Checkpoint">001B77</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001B77</idno><idno type="wicri:doubleKey">0302-9743:2002:Garcia Diaz M:solving:mixed:quantified</idno><idno type="wicri:Area/Main/Merge">008B97</idno><idno type="wicri:Area/Main/Curation">008741</idno><idno type="wicri:Area/Main/Exploration">008741</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Solving Mixed Quantified Constraints over a Domain Based on <formula xml:id="IEq1" notation="TEX"><media mimeType="image" url=""></media>$$
\mathcal{R}
$$
</formula>eal Numbers and <formula xml:id="IEq2" notation="TEX"><media mimeType="image" url=""></media>$$
\mathcal{H}
$$
</formula>erbrand Terms</title><author><name sortKey="Garcia Diaz, Miguel" sort="Garcia Diaz, Miguel" uniqKey="Garcia Diaz M" first="Miguel" last="García-Díaz">Miguel García-Díaz</name><affiliation wicri:level="3"><country>Espagne</country><placeName><settlement type="city">Madrid</settlement><region nuts="2" type="region">Communauté de Madrid</region></placeName><wicri:orgArea>Dpto. Sistemas Informáticos y Programación, Universidad Complutense de Madrid</wicri:orgArea></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Espagne</country></affiliation></author><author><name sortKey="Nieva, Susana" sort="Nieva, Susana" uniqKey="Nieva S" first="Susana" last="Nieva">Susana Nieva</name><affiliation wicri:level="3"><country>Espagne</country><placeName><settlement type="city">Madrid</settlement><region nuts="2" type="region">Communauté de Madrid</region></placeName><wicri:orgArea>Dpto. Sistemas Informáticos y Programación, Universidad Complutense de Madrid</wicri:orgArea></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Espagne</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Combining the logic of hereditary Harrop formulas HH with a constraint system, a logic programming language is obtained that extends Horn clauses in two different directions, thus enhancing substantially the expressivity of Prolog. The implementation of this new language requires the ability to test the satisfiability of constraints built up by means of terms and predicates belonging to the domain of the chosen constraint system, and by the connectives and quantifiers usual in first-order logic. In this paper we present a constraint system called $$ \mathcal{R}\mathcal{H} $$ for a hybrid domain that mixes Herbrand terms and real numbers. It arises when joining the axiomatization of the arithmetic of real numbers and the axiomatization of the algebra of finite trees. We have defined an algorithm to solve certain constraints of this kind. The novelty relies on the combination of two different mechanisms, based on elimination of quantifiers, o ne used for solving unification and disunification problems, the other used to solve polynomials. This combination provides a procedure to solve $$ \mathcal{R}\mathcal{H} $$ -constraints in the context of HH with constraints.</div></front></TEI><affiliations><list><country><li>Espagne</li></country><region><li>Communauté de Madrid</li></region><settlement><li>Madrid</li></settlement></list><tree><country name="Espagne"><region name="Communauté de Madrid"><name sortKey="Garcia Diaz, Miguel" sort="Garcia Diaz, Miguel" uniqKey="Garcia Diaz M" first="Miguel" last="García-Díaz">Miguel García-Díaz</name></region><name sortKey="Garcia Diaz, Miguel" sort="Garcia Diaz, Miguel" uniqKey="Garcia Diaz M" first="Miguel" last="García-Díaz">Miguel García-Díaz</name><name sortKey="Nieva, Susana" sort="Nieva, Susana" uniqKey="Nieva S" first="Susana" last="Nieva">Susana Nieva</name><name sortKey="Nieva, Susana" sort="Nieva, Susana" uniqKey="Nieva S" first="Susana" last="Nieva">Susana Nieva</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 008741 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 008741 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:41410A90B5254E892607C6E4FF45F4FAC578309C
|texte= Solving Mixed Quantified Constraints over a Domain Based on $$\mathcal{R}$$eal Numbers and $$\mathcal{H}$$erbrand Terms
}}
| This area was generated with Dilib version V0.6.33. |  |